import Yices hiding (and, or, not)
import qualified Yices as Y

-- Typedefs for readability
type Stone = Int
type Column = Int
type Row = Int
type Bit = Int

-- Size of the board
n = 11

-- board
b' :: Ident (Row -> Column -> Bool)
(b',b) = ident2 "b"

-- The main script
formula = conj $
    -- Exactly one stone in a row/column
    [ conj [singleton (b s) /\ singleton (flip b s) | s <- [1..n]]
    -- Distance between stones > sqrt(6)
    , conj [non (b i j /\ b i' j')
           | i <- [1..n], j <- [1..n], i' <- [i-2..i+2], j' <- [j-2..j+2]
           , i' >= 1, i' <= n, j' >= 1, j' <= n, i /= i', j /= j'
           , (i-i')^2 + (j-j')^2 <= 6
           ]
    -- Predefined forbidden zones
    , conj . concat $
        [ [non (b  2 j) | j <- [1..5]]
        , [non (b  i 4) | i <- [4..8]] 
        , [non (b 10 j) | j <- [4..11]]
        , [non (b  i j) | i <- [2..8], j <- [7..8]]
        ]
    ]
  where
    singleton p = disj [p i | i <- [1..n]] /\ maxone p
    maxone p = conj [non (p i /\ p j) | i <- [2..n], j <- [1..i-1]]

main = bdd -- or "yices", as you wish
  where
    yices = printScript [ define b', assert formula ]
    bdd = printBddSat formula
